$\forall$$M$:MsgA, $k$:Knd, $s$:$M$.state, $v$:$M$.da($k$).
\\[0ex]$\neg$ma{-}has{-}sends($M$;$k$) $\Rightarrow$ $M$.sends($k$,$s$,$v$) $=$ nil $\in$ $M$.Msg List